ds1,ds2:fpf(Id; x.Type).
fpf-sub(Id; x.Type; id-deq; ds2; ds1)  subtype_rel(decl-state(ds1); decl-state(ds2)) 

latex

Definitions	Id, Type, top, fpf-cap(f; eq; x; z), x:A. B(x), x. t(x), t  T, x.A(x), P  Q, decl-state(ds), fpf(A; a.B(a)), id-deq, fpf-sub(A; a.B(a); eq; f; g), x:A  B(x), b, s = t, atom{$n:n}, <a, b>, True, T, x:AB(x), f(a), x(s), EqDecider(T)
Lemmas	squash wf, true wf, deq wf, subtype-fpf-cap-top, fpf-sub wf, id-deq wf, fpf wf, Id wf, subtype rel dep function, top wf, fpf-cap wf, subtype rel self